\begin{tabbing}
ESAxioms(\=$E$;$T$;$M$;\+
\\[0ex]${\it loc}$;${\it kind}$;${\it val}$;
\\[0ex]${\it when}$;${\it after}$;
\\[0ex]${\it sends}$;${\it sender}$;${\it index}$;
\\[0ex]${\it first}$;${\it pred}$;
\\[0ex]${\it causl}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$, ${\it e'}$:$E$. ${\it loc}$($e$) $=$ ${\it loc}$(${\it e'}$) $\Rightarrow$ ${\it causl}$($e$,${\it e'}$) $\vee$ $e$ $=$ ${\it e'}$ $\vee$ ${\it causl}$(${\it e'}$,$e$))\+
\\[0ex]\& ($\forall$$e$:$E$. ${\it first}$($e$) $\Leftrightarrow$ ($\forall$${\it e'}$:$E$. ${\it loc}$(${\it e'}$) $=$ ${\it loc}$($e$) $\Rightarrow$ $\neg$${\it causl}$(${\it e'}$,$e$)))
\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]$\neg$${\it first}$($e$)
\\[0ex]$\Rightarrow$ \=${\it loc}$(${\it pred}$($e$)) $=$ ${\it loc}$($e$) \& ${\it causl}$(${\it pred}$($e$),$e$)\+
\\[0ex]\& ($\forall$${\it e'}$:$E$. ${\it loc}$(${\it e'}$) $=$ ${\it loc}$($e$) $\Rightarrow$ $\neg$(${\it causl}$(${\it pred}$($e$),${\it e'}$) \& ${\it causl}$(${\it e'}$,$e$))))
\-\-\\[0ex]\& ($\forall$$e$:$E$. $\neg$${\it first}$($e$) $\Rightarrow$ ($\forall$$x$:Id. ${\it when}$($x$,$e$) $=$ ${\it after}$($x$,${\it pred}$($e$))))
\\[0ex]\& (Trans $e$,${\it e'}$:$E$. ${\it causl}$($e$,${\it e'}$))
\\[0ex]\& SWellFounded(${\it causl}$($e$,${\it e'}$))
\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]isrcv(${\it kind}$($e$))
\\[0ex]$\Rightarrow$ \=(${\it sends}$(lnk(${\it kind}$($e$)),${\it sender}$($e$)))[${\it index}$($e$)]\+
\\[0ex]$=$
\\[0ex]msg(lnk(${\it kind}$($e$));tag(${\it kind}$($e$));${\it val}$($e$)))
\-\-\\[0ex]\& ($\forall$$e$:$E$. isrcv(${\it kind}$($e$)) $\Rightarrow$ ${\it causl}$(${\it sender}$($e$),$e$))
\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:$E$.\+
\\[0ex]${\it causl}$($e$,${\it e'}$)
\\[0ex]$\Rightarrow$ \=$\neg$${\it first}$(${\it e'}$) \& ${\it causl}$($e$,${\it pred}$(${\it e'}$)) $\vee$ $e$ $=$ ${\it pred}$(${\it e'}$)\+
\\[0ex]$\vee$ isrcv(${\it kind}$(${\it e'}$)) \& ${\it causl}$($e$,${\it sender}$(${\it e'}$)) $\vee$ $e$ $=$ ${\it sender}$(${\it e'}$))
\-\-\\[0ex]\& ($\forall$$e$:$E$. isrcv(${\it kind}$($e$)) $\Rightarrow$ ${\it loc}$($e$) $=$ destination(lnk(${\it kind}$($e$))))
\\[0ex]\& ($\forall$$e$:$E$, $l$:IdLnk. $\neg$${\it loc}$($e$) $=$ source($l$) $\Rightarrow$ ${\it sends}$($l$,$e$) $=$ nil)
\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:$E$.\+
\\[0ex]isrcv(${\it kind}$($e$))
\\[0ex]$\Rightarrow$ isrcv(${\it kind}$(${\it e'}$))
\\[0ex]$\Rightarrow$ lnk(${\it kind}$($e$)) $=$ lnk(${\it kind}$(${\it e'}$))
\\[0ex]$\Rightarrow$ (\=${\it causl}$($e$,${\it e'}$)\+
\\[0ex]$\Leftrightarrow$
\\[0ex]${\it causl}$(${\it sender}$($e$),${\it sender}$(${\it e'}$)) $\vee$ ${\it sender}$($e$) $=$ ${\it sender}$(${\it e'}$) \& ${\it index}$($e$)$<$${\it index}$(${\it e'}$)))
\-\-\\[0ex]\& (\=$\forall$$e$:$E$, $l$:IdLnk, $n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it sends}$($l$,$e$)$\parallel$}}$.\+
\\[0ex]$\exists$${\it e'}$:$E$. isrcv(${\it kind}$(${\it e'}$)) \& lnk(${\it kind}$(${\it e'}$)) $=$ $l$ \& ${\it sender}$(${\it e'}$) $=$ $e$ \& ${\it index}$(${\it e'}$) $=$ $n$)
\-\-
\end{tabbing}